es:event_system{i:l}, e3,e2,e1:es-E(es).
es-le(es; e1; e2)
 es-le(es; e1; e3)
 (iseg(es-E(es); [e1, e2]; [e1, e3])  es-le(es; e2; e3)) 

latex

Definitions

x:A. B(x), P  Q, t  T, prop{i:l}, x. t(x), P  Q, P  Q, P  Q, es-le(es; e; e'), P  Q, guard(T), A c B, A, T, True, wellfounded{i:l}(A; x,y.R(x;y)), x(s), es-locl(es; e; e'), False

Lemmas

es-locl-wellfnd, es-E wf, es-le wf, iff wf, iseg wf, es-interval wf, es-locl wf, event system wf, es-le-iff, es-pred wf, es-pred-locl, es-interval-less, es-le-pred, iff functionality wrt iff, or functionality wrt iff, iseg append single, es-locl transitivity1, es-interval-one-one, es-interval-eq, es-le-not-locl, es-le-loc, es-loc wf, squash wf, true wf, member-es-interval, es-le weakening eq, iseg member, member singleton, es-loc-pred, es-locl-iff, not wf, assert wf, es-first wf, iseg weakening